﻿/*============================================
 * 类名 :ProveLow
 * 描述 :这个类用来存储推理的运算定律
 *   
 * 创建时间: 2009-11-3 16:03:26
 *============================================*/
using System;
using System.Collections.Generic;

using System.Text;

namespace 命题证明
{
    /// <summary>推理的运算定律，相当于一个参数</summary> 
    class Law
    {
        /// <summary>运算定律</summary>
        /// <param name="condition">中序形式的条件表达式</param>
        /// <param name="result">中序形式的结论</param>
        /// <param name="name">这个运算定律的名称</param>
        public Law( string condition, string result, string name )
        {
            this.condition = new Expression( condition );
            //middle = condition;
            //this.Result = new Expression( result );           
            this.Name = name;
            CreateAfters( ExpressionFactory.MiddleToAfter( result ) );
        }

        public Law( LawFormat format, string name )
        {
            allFormats.Add( format );
            this.Name = name;
        }

        #region "变量区"

        List<LawFormat> allFormats = new List<LawFormat>();

        /// <summary>这个公式所有的全等的后序形式</summary>
        public List<LawFormat> AllFormats
        {
            get { return allFormats; }
            set { allFormats = value; }
        }
        /// <summary>这个运算定律的名称</summary>
        public string Name { get; set; }

        /// <summary>定律的前提</summary>
        Expression condition;

        #endregion

        //创建所有的后序形式
        void CreateAfters( string result )
        {
            //所有可交换的节点
            List<OperatorNode> canChange = FindChang();
            List<char> addNot = FindNot();
            //这里又一次地用到了这个二进制数类
            BinaryNumber bin = new BinaryNumber( canChange.Count + addNot.Count );
            for ( int i = 0; i <= bin.Max; i++ )
            {
                bin.DecimalNumber = i;
                //交换过的节点索引
                List<int> chengedIndex = new List<int>();
                List<int> addNotIndex = new List<int>();
                for ( int j = 0; j < canChange.Count; j++ )
                {
                    if ( bin.Binary[j] )
                    {
                        //先交换，并将交换后的节点记录下来
                        ChangeNode( canChange[j] );
                        chengedIndex.Add( j );
                    }
                }
                string newResult = result;
                for ( int j = 0; j < bin.Binary.Count - canChange.Count; j++ )
                {
                    if ( bin.Binary[canChange.Count + j] )
                    {
                        AddNot( addNot[j] );
                        addNotIndex.Add( j );
                        newResult = newResult.Replace( addNot[j].ToString(), addNot[j].ToString() + Operator.Not.ToString() );
                    }
                }
                string t = ExpressionFactory.ConvertToAfter( condition.Head );
                int len = t.Length;
                //这里用的不是双重否定律，而是在生成公式
                do
                {
                    len = t.Length;
                    t = t.Replace( "┐┐", "" );
                } while ( len > t.Length );


                allFormats.Add( new LawFormat( t, newResult ) );
                //afterExpressions.Add( );
                //将交换后的节点还原回来
                foreach ( int index in chengedIndex )
                {
                    ChangeNode( canChange[index] );
                }
                foreach ( int index in addNotIndex )
                {
                    RemoveNot( addNot[index] );
                }
            }
        }

        void AddNot( char p )
        {
            foreach ( WordNode i in condition.WordNodes )
            {
                if ( i.Word == p )
                {
                    OperatorNode n = new OperatorNode( Operator.Not );
                    if ( i.Parent.Right == i )
                    {
                        i.Parent.Right = n;
                        n.Parent = i.Parent;
                        n.Right = i;
                        i.Parent = n;
                    }
                    else
                    {
                        i.Parent.Left = n;
                        n.Parent = i.Parent;
                        n.Right = i;
                        i.Parent = n;
                    }
                }
            }
        }

        void RemoveNot( char ch )
        {
            foreach ( WordNode i in condition.WordNodes )
            {
                if ( i.Word == ch )
                {
                    if ( i.Parent.Parent.Right == i.Parent )
                    {
                        Node t = i.Parent;
                        t.Parent.Right = i;
                        i.Parent = t.Parent;
                    }
                    else
                    {
                        Node t = i.Parent;
                        t.Parent.Left = i;
                        i.Parent = t.Parent;
                    }
                }

            }
        }

        List<OperatorNode> FindChang()
        {
            List<OperatorNode> canChange = new List<OperatorNode>();
            foreach ( OperatorNode op in condition.OperatorNodes )
            {
                if ( op.Operator == Operator.And || op.Operator == Operator.Or || op.Operator == Operator.ProveTwo )
                {
                    canChange.Add( op );
                }
            }
            return canChange;
        }

        //(a∨b)∧┐b 找到这种表达式里所有的b节点
        List<char> FindNot()
        {
            List<char> addNot = new List<char>();
            foreach ( WordNode op in condition.WordNodes )
            {
                if ( op.Parent is OperatorNode && ( op.Parent as OperatorNode ).Operator == Operator.Not )
                {
                    foreach ( WordNode p in condition.WordNodes )
                    {
                        if ( p.Word == op.Word && p.Parent is OperatorNode && ( p.Parent as OperatorNode ).Operator != Operator.Not )
                        {
                            if ( !addNot.Exists( delegate( char w ) {
                                if ( w == p.Word )
                                    return true;
                                return false;
                            } ) )
                                addNot.Add( p.Word );
                            break;
                        }
                    }
                }
            }
            return addNot;
        }

        void ChangeNode( OperatorNode op )
        {
            Node temp;
            temp = op.Left;
            op.Left = op.Right;
            op.Right = temp;
        }

    }
}
